(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r7 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const r12 Real)
(assert (and v1 v1 v0 v0 v1 v1 v0 v0))
(assert (=> (>= r9 r3 r4 r10 6011833.0) v1))
(assert v0)
(declare-const v2 Bool)
(check-sat)
(declare-const v3 Bool)
(assert (>= 2261177.0 r3 r9))
(push)
(pop)
(declare-const v4 Bool)
(assert (exists ((q3 Real) (q4 Bool)) (=> (and v0 (=> (>= r9 r3 r4 r10 6011833.0) v1) q4 q4 q4) (< r10 q3))))
(assert (>= r9 r3 r4 r10 6011833.0))
(check-sat)
(assert (forall ((q5 Bool) (q6 Real) (q7 Real)) (not (>= q7 (/ 2261177.0 6011833.0)))))
(assert (and (=> v4 v1) (<= r4 (/ 2261177.0 6011833.0) 2261177.0 (* r3 r1)) v4 (>= r9 r3 r4 r10 6011833.0) v2 (<= r4 (/ 2261177.0 6011833.0) 2261177.0 (* r3 r1)) v1 (>= r9 r3 r4 r10 6011833.0) (=> (>= r9 r3 r4 r10 6011833.0) v1) v2 (=> v4 v1)))
(check-sat)
